PEARL[1]

Constable, Cornell University, 80's

A language for doing constructive mathematics.